a, b:.  :{0..a}  {0..b} ~ {0..(a * b)} 

latex

Definitions	{i..j}, x:A  B(x), Bij(A;B;f), {x:A| B(x)} , , , t  T, a < b, P  Q, False, A, P & Q, A  B, i  j < k, Void, x:AB(x), x:A. B(x), x:A. B(x),  A ~ B, n * m, n+m, let x,y = A in B(x;y), x.A(x), #$n, n - m, s = t, , Surj(A;B;f), Inj(A;B;f), Div(a;n;q), <a, b>, {T}, SQType(T), s ~ t, True, T, -n, left + right, P  Q, Dec(P), n rem m, n  m,
Lemmas	decidable lt, div rem sum, rem bounds 1, decidable int equal, le wf, div unique, mul bounds 1a, mul preserves le